/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package chameleon.model.NuGatManager.Strategy;

import chameleon.model.NuGatStructure.game.GameParams;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.opt.OptGame;
import chameleon.model.NuGatStructure.strategy.StructCheckLTLGameSF07;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.game.Game;

/**
 *
 * @author simon
 */
public class LtlGameSFO7Computation {    
     
    private PropGame prop_;
    private NuGatInterface nugat_;
    private int kmin_;
    private int kmax_;
    private int w;
    private GameParams params_;
    private Game game_;

    public LtlGameSFO7Computation(PropGame prop_,Game game, NuGatInterface nugat_) {
        this.prop_ = prop_;
        this.nugat_ = nugat_;
        this.kmin_ = 0;
        this.kmax_ = 20;
        this.w = nugat_.GAME_WHO_BOTH;
        params_ = new GameParams(1,0, 1, "test", nugat_);
        game_=game;
    }

    public void setKmax_(int kmax_) {
        this.kmax_ = kmax_;
    }

    public void setKmin_(int kmin_) {
        this.kmin_ = kmin_;
    }

    public void setW(int w) {
        this.w = w;
    }

    
    
    
    public StructCheckLTLGameSF07 checkLtlGameSF07(){
          StructCheckLTLGameSF07 cls;
          int curr_k;
          int curr_player;
          boolean done;
          OptGame opt = game_.getOptsHandlerInstance();

          /*PROP_GAME_CHECK_INSTANCE(prop);*/
          if(!(prop_.getStatus() == nugat_.Prop_Unchecked))
              throw new RuntimeException("checkLtlGameSFO07 line 45 : prop is not unchecked");
          if(!(0 <= kmin_))
              throw new RuntimeException("checkLtlGameSF07 line 47 : kmin < 0");
          if (!(kmin_ <= kmax_))
              throw new RuntimeException("checkLtlGameSFO07 line 49: kmin > kmax");
         if(!((w == nugat_.GAME_WHO_BOTH) ||
                       (w == nugat_.GAME_WHO_PROTAGONIST) ||
                       (w == nugat_.GAME_WHO_ANTAGONIST) ||
                       (w == nugat_.GAME_WHO_PLAYER_1) ||
                       (w == nugat_.GAME_WHO_PLAYER_2)))
             throw new RuntimeException("checkLtlGameSFO07 line 55: uncorrect Game_Who");
          if(!(opt.gameInitialCondition() ==
                       'N'))
              throw new RuntimeException("checkLtlGameSFO07 line 58: uncorrect initial condition");

          cls = new StructCheckLTLGameSF07(prop_, params_, kmin_, kmax_, w, nugat_);

          /* As in gameGeneral.c::Game_BeforeCheckingSpec. */
          /*if (nugat_.opt_verbose_level_ge(nugat_.OptsHandler_get_instance(), 1)) {
            fprintf(nusmv_stderr, "computing ");
            fprintf(nusmv_stderr, " ");
            Prop_print(PROP(cls->prop), nusmv_stderr);
            fprintf(nusmv_stderr, "\n");
          }

          /* Some additional info. */
          /*if (opt_verbose_level_ge(OptsHandler_get_instance(), 2)) {
            fprintf(nusmv_stderr,
               "\nwith Game_CheckLtlGameSpecSF07 using kmin = %d, kmax = %d, w = %s.\n",
                    cls->kmin,
                    cls->kmax,
                    Game_Who_to_string(cls->w));
          }

          /* The main loop. */
          curr_k = kmin_;
          done = false;
          
          while ((!done) && (curr_k <= kmax_)) {
            if (((w == nugat_.GAME_WHO_PROTAGONIST) && (cls.getPlayer().isPLayer1())) ||
                ((w == nugat_.GAME_WHO_ANTAGONIST) && (cls.getPlayer().isPLayer2())) ||
                ((w == nugat_.GAME_WHO_BOTH) && (cls.getPlayer().isPLayer1())) ||
                (w == nugat_.GAME_WHO_PLAYER_1)) {
              curr_player = nugat_.PLAYER_1;
            } else {
              curr_player = nugat_.PLAYER_2;
            }
            
            nugat_.Game_SF07_StructCheckLTLGameSF07_run_iteration(cls.ptr(), curr_k, curr_player);
            
            PropGame prop = cls.getProp();
                    
            if ((prop.getStatus() == nugat_.Prop_True) ||
                (prop.getStatus() == nugat_.Prop_False)) {
              done = true;
            }
            
            if ((!done) && (w == nugat_.GAME_WHO_BOTH)) {
              if (curr_player == nugat_.PLAYER_1) {
                curr_player = nugat_.PLAYER_2;
              } else {
                curr_player = nugat_.PLAYER_1;
              }
              nugat_.Game_SF07_StructCheckLTLGameSF07_run_iteration(cls.ptr(), curr_k, curr_player);
              
              prop = cls.getProp();
              if ((prop.getStatus() == nugat_.Prop_True) ||
                (prop.getStatus() == nugat_.Prop_False)) {
                done = true;
              }
            }

            if (!done) {
              curr_k++;
            }
          }
        
        /*PropGame prop = cls.getProp();
        GameStrategy strategy = cls.getStrategy();
        strategy.setStatus(prop.getStatus());
        strategy.setProp(prop_);*/
          
          
        return cls;
    }
    
}
